COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	PROVER is an implementation of a resolution-based first-order theorem
C00004 ENDMK
C⊗;
PROVER is an implementation of a resolution-based first-order theorem
prover.   The basic philosphy and the  structure of this program were
described  in  "An  Interactive  Theorem-proving  Program",  Allen  &
Luckham,  MI5  (1970); SAILON-73  is  a  user's  manual and  gives  a
detailed  description of the  latest system. Essentially  the user is
supplied  with  a  reasonably  standard  mathematical   notation  for
specifying  the problem  and  a simple  language  for describing  the
strategies to  guide the  proof.   The user  may interrupt  the proof
search at any  time and use  the on-line facilities to  further guide
the  prover. The on-line  editor allows  the user to  associate names
with collections  of  deductions.    The collecting  can  be  done by
pattern matching or by explicit user-selection. These collections can
then  be used by:  commands to  modify the current  set of deductions
(delete,  simplify  by  ...);  rules  of  inference  (resolution,  or
paramodulation); or by commands to initiate sub-proofs.